%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Todos los días los empleados de una empresa se encuentran en la cafetería,
% en la sala de descanso o en el aparcamiento. Todos los que han coincidido con
% Andrés en el parking se han encontrado con alguien en la sala de descanso.
% Nadie ha coincidido con Juan en la sala de descanso. Andrés se ha encontrado
% en el parking con todos los que han coincidido con Daniel en la cafetería.
% Por tanto Juan se ha encontrado en el parking con Daniel."

%==============================================================================
% Formalización
%==============================================================================

set(binary_res).

formula_list(sos).
% Todos los días los empleados de una empresa se encuentran en la cafetería, en
% la sala de descanso o en el aparcamiento.
  all x y (c(x,y) | p(x,y) | d(x,y)).

  all x y (c(x,y) -> c(y,x)).
  all x y (p(x,y) -> p(y,x)).
  all x y (d(x,y) -> d(y,x)).

% Todos los que han coincidido con Andrés en el parking se han encontrado con
% alguien en la sala de descanso.
  all x exists y (p(Andres,x) -> d(x,y)).

% Nadie ha coincidido con Juan en la sala de descanso.
  - (exists x (d(x,Juan))).

% Andrés se ha encontrado en el parking con todos los que han coincidido con
% Daniel en la cafetería.
  all x (c(Daniel,x) -> p(Andres,x)).

% Conclusión: Juan se ha encontrado en el parking con Daniel.
  - p(Juan,Daniel).

end_of_list.

%==============================================================================
